(set-logic QF_BV)
(set-option :opt.priority lex)
(set-option :opt.maxsat_engine wmax)
(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const v4 Bool)
(declare-const v5 Bool)
(declare-const v6 Bool)
(declare-const v7 Bool)
(declare-const v8 Bool)
(declare-const v9 Bool)
(declare-const v10 Bool)
(declare-const bv_9-0 (_ BitVec 9))
(declare-const v11 Bool)
(declare-const bv_3-0 (_ BitVec 3))
(declare-const v12 Bool)
(declare-const v13 Bool)
(declare-const v14 Bool)
(declare-const v15 Bool)
(declare-const v16 Bool)
(declare-const v17 Bool)
(declare-const v18 Bool)
(declare-const v19 Bool)
(assert (or (distinct #b1100111010 #b1100111010) (bvugt ((_ rotate_right 4) bv_3-0) bv_3-0) (distinct #b1100111010 #b1100111010)))
(assert (or v1 (distinct #b1100111010 #b1100111010) (= ((_ rotate_right 4) bv_3-0) bv_3-0)))
(assert (or v14 v14 v6))
(assert (or v18 (bvugt ((_ rotate_right 4) bv_3-0) bv_3-0) v10))
(assert (or v18 (distinct #b1100111010 #b1100111010) (bvugt ((_ rotate_right 4) bv_3-0) bv_3-0)))
(assert (or (bvule #b01000100001 #b01000100001) v8 v16))
(assert (or v7 v8 v18))
(assert (or v6 v0 v18))
(assert (or v14 (= ((_ rotate_right 4) bv_3-0) bv_3-0) v16))
(assert (or v6 v7 v18))
(assert (or v18 v16 v1))
(assert (or v18 (bvugt ((_ rotate_right 4) bv_3-0) bv_3-0) v6))
(assert (or (distinct #b1100111010 #b1100111010) v0 v14))
(assert (or v0 (bvugt ((_ rotate_right 4) bv_3-0) bv_3-0) v10))
(assert (or v0 v7 (bvule #b01000100001 #b01000100001)))
(assert (or v14 (= v13 v6 v7 v10 v11) v1))
(assert (or (bvule #b01000100001 #b01000100001) v7 v16))
(assert (or (= ((_ rotate_right 4) bv_3-0) bv_3-0) v14 v1))
(assert (or v18 (distinct #b1100111010 #b1100111010) v8))
(assert (or v7 v10 v16))
(assert (or v10 v7 v10))
(assert (or v16 (distinct #b1100111010 #b1100111010) v6))
(assert (or v18 v8 v16))
(assert (or v6 v6 v6))
(assert (or (= v13 v6 v7 v10 v11) v0 v6))
(assert (or v8 v7 v7))
(assert (or (distinct #b1100111010 #b1100111010) v0 (= v13 v6 v7 v10 v11)))
(assert (or (= v13 v6 v7 v10 v11) v0 (= ((_ rotate_right 4) bv_3-0) bv_3-0)))
(assert (or v1 (bvugt ((_ rotate_right 4) bv_3-0) bv_3-0) (= ((_ rotate_right 4) bv_3-0) bv_3-0)))
(assert (or (= v13 v6 v7 v10 v11) v7 v6))
(assert (or v8 v10 v6))
(assert (or (bvule #b01000100001 #b01000100001) v18 (bvugt ((_ rotate_right 4) bv_3-0) bv_3-0)))
(assert (or (bvugt ((_ rotate_right 4) bv_3-0) bv_3-0) (= ((_ rotate_right 4) bv_3-0) bv_3-0) v16))
(assert (or v1 v8 v0))
(assert (or (= v13 v6 v7 v10 v11) (= ((_ rotate_right 4) bv_3-0) bv_3-0) (bvule #b01000100001 #b01000100001)))
(assert (or (= v13 v6 v7 v10 v11) v10 (= ((_ rotate_right 4) bv_3-0) bv_3-0)))
(assert (or (= v13 v6 v7 v10 v11) v14 v8))
(assert (or v14 (= ((_ rotate_right 4) bv_3-0) bv_3-0) v18))
(assert (or (bvule #b01000100001 #b01000100001) v14 v16))
(assert (or v18 (= v13 v6 v7 v10 v11) (bvugt ((_ rotate_right 4) bv_3-0) bv_3-0)))
(assert (or v7 (bvugt ((_ rotate_right 4) bv_3-0) bv_3-0) v1))
(assert (or v1 v16 (= ((_ rotate_right 4) bv_3-0) bv_3-0)))
(assert (or v18 v16 v1))
(assert (or v7 v8 v18))
(assert (or v14 (= ((_ rotate_right 4) bv_3-0) bv_3-0) v16))
(assert (and (or v14 (= ((_ rotate_right 4) bv_3-0) bv_3-0) v16) (or (= v13 v6 v7 v10 v11) v10 (= ((_ rotate_right 4) bv_3-0) bv_3-0)) (or (= v13 v6 v7 v10 v11) (= ((_ rotate_right 4) bv_3-0) bv_3-0) (bvule #b01000100001 #b01000100001)) (or v18 v16 v1) (or (bvule #b01000100001 #b01000100001) v8 v16) (or v0 v7 (bvule #b01000100001 #b01000100001))))
(assert (=> (or v7 v8 v18) (or (distinct #b1100111010 #b1100111010) v0 (= v13 v6 v7 v10 v11))))
(assert (or (and (or v14 (= ((_ rotate_right 4) bv_3-0) bv_3-0) v16) (or (= v13 v6 v7 v10 v11) v10 (= ((_ rotate_right 4) bv_3-0) bv_3-0)) (or (= v13 v6 v7 v10 v11) (= ((_ rotate_right 4) bv_3-0) bv_3-0) (bvule #b01000100001 #b01000100001)) (or v18 v16 v1) (or (bvule #b01000100001 #b01000100001) v8 v16) (or v0 v7 (bvule #b01000100001 #b01000100001))) (or v8 v10 v6)))
(assert (=> (or v18 (= v13 v6 v7 v10 v11) (bvugt ((_ rotate_right 4) bv_3-0) bv_3-0)) (or (distinct #b1100111010 #b1100111010) (bvugt ((_ rotate_right 4) bv_3-0) bv_3-0) (distinct #b1100111010 #b1100111010))))
(assert (or (or (= v13 v6 v7 v10 v11) v10 (= ((_ rotate_right 4) bv_3-0) bv_3-0)) (or v1 (distinct #b1100111010 #b1100111010) (= ((_ rotate_right 4) bv_3-0) bv_3-0))))
(assert (or v8 v10 v6))
(minimize bv_3-0)
(minimize bv_9-0)
(check-sat)
(exit)
